Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(nil,YS)  → YS
2:    app(cons(X,XS),YS)  → cons(X,n__app(activate(XS),YS))
3:    from(X)  → cons(X,n__from(n__s(X)))
4:    zWadr(nil,YS)  → nil
5:    zWadr(XS,nil)  → nil
6:    zWadr(cons(X,XS),cons(Y,YS))  → cons(app(Y,cons(X,n__nil)),n__zWadr(activate(XS),activate(YS)))
7:    prefix(L)  → cons(nil,n__zWadr(L,n__prefix(L)))
8:    app(X1,X2)  → n__app(X1,X2)
9:    from(X)  → n__from(X)
10:    s(X)  → n__s(X)
11:    nil  → n__nil
12:    zWadr(X1,X2)  → n__zWadr(X1,X2)
13:    prefix(X)  → n__prefix(X)
14:    activate(n__app(X1,X2))  → app(activate(X1),activate(X2))
15:    activate(n__from(X))  → from(activate(X))
16:    activate(n__s(X))  → s(activate(X))
17:    activate(n__nil)  → nil
18:    activate(n__zWadr(X1,X2))  → zWadr(activate(X1),activate(X2))
19:    activate(n__prefix(X))  → prefix(activate(X))
20:    activate(X)  → X
There are 18 dependency pairs:
21:    APP(cons(X,XS),YS)  → ACTIVATE(XS)
22:    ZWADR(cons(X,XS),cons(Y,YS))  → APP(Y,cons(X,n__nil))
23:    ZWADR(cons(X,XS),cons(Y,YS))  → ACTIVATE(XS)
24:    ZWADR(cons(X,XS),cons(Y,YS))  → ACTIVATE(YS)
25:    PREFIX(L)  → NIL
26:    ACTIVATE(n__app(X1,X2))  → APP(activate(X1),activate(X2))
27:    ACTIVATE(n__app(X1,X2))  → ACTIVATE(X1)
28:    ACTIVATE(n__app(X1,X2))  → ACTIVATE(X2)
29:    ACTIVATE(n__from(X))  → FROM(activate(X))
30:    ACTIVATE(n__from(X))  → ACTIVATE(X)
31:    ACTIVATE(n__s(X))  → S(activate(X))
32:    ACTIVATE(n__s(X))  → ACTIVATE(X)
33:    ACTIVATE(n__nil)  → NIL
34:    ACTIVATE(n__zWadr(X1,X2))  → ZWADR(activate(X1),activate(X2))
35:    ACTIVATE(n__zWadr(X1,X2))  → ACTIVATE(X1)
36:    ACTIVATE(n__zWadr(X1,X2))  → ACTIVATE(X2)
37:    ACTIVATE(n__prefix(X))  → PREFIX(activate(X))
38:    ACTIVATE(n__prefix(X))  → ACTIVATE(X)
The approximated dependency graph contains one SCC: {21-24,26-28,30,32,34-36,38}.
Tyrolean Termination Tool  (13.20 seconds)   ---  May 3, 2006